A  B
== if Rnone?(A) True
== i; Rplus?(A) Rplus-left(A)  B & Rplus-right(A)  B
== i; Rplus?(B) A  Rplus-left(B)  A  Rplus-right(B)
== else A = B fi
(recursive) 

latex

---

clarification:

R-sub{i:l}
R-sub(A; B)
== if Rnone?(A) True
== i; Rplus?(A) R-sub{i:l}(Rplus-left(A); B) & R-sub{i:l}(Rplus-right(A); B)
== i; Rplus?(B) R-sub{i:l}(A; Rplus-left(B))  R-sub{i:l}(A; Rplus-right(B))
== else A = B  es_realizer{i:l} fi
(recursive) 

latex

Definitions	Y, x.A(x), Rnone?(x1), True, P & Q, if b t else f fi, Rplus?(x1), P  Q, Rplus-left(x1), f(a), Rplus-right(x1), s = t, Realizer
FDL editor aliases	R-sub